1. Technical Field
The present invention relates in general to representing logic functions and in particular to representing a logic function in a decision diagram. Still more particularly, the present invention relates to a system, method and computer program product for building decision diagrams efficiently in a structural network representation of a digital circuit, using a dynamic, resource-constrained and interleaved depth-first-search and modified breadth-first-search schedule.
2. Description of the Related Art
Many tasks in computer-aided design (CAD), such as equivalence checking, property checking, logic synthesis and false-paths analysis require Boolean reasoning and analysis on problems derived from representations of circuit structures. One commonly-used approach to Boolean reasoning and analysis for applications operating on representations of circuit structures is to represent the underlying logical problem structurally (as a circuit graph), and then use Binary Decision Diagrams (BDDs) to convert the structural representation into a functionally canonical form.
In such an approach, in which a logical problem is represented structurally and binary decision diagrams are used to convert the structural representation into a functionally canonical form, a set of nodes for which binary decision diagrams are required to be built, called “sink” nodes, are identified. Examples of sink nodes include the output node or nodes in an equivalence checking or a false-paths analysis context. Examples of sink nodes also include targets in a property-checking or model-checking context.
Following identification of the sink nodes, binary decision diagrams for these nodes are built in a topological manner, starting at the input variables for a function. The process of building binary decision diagrams flows from input variables to intermediate nodes in the circuit graph representation until, finally, the binary decision diagrams for the sink nodes are built.
Binary decision diagrams provide an effective tool for Boolean reasoning and analysis in applications operating on representations of circuit structures, but binary decision diagrams frequently suffer from exponential space complexity and associated resource (e.g. memory) consumption. In the worst case, exponential complexity and associated resource consumption preclude completion of binary decision diagrams.
One reason for resource consumption problems in constructing binary decision diagrams relates to reliance on a total order in the Boolean variables in the binary decision diagrams. Another reason that the construction of binary decision diagrams is memory intensive relates to the sheer number of binary decision diagrams that are “alive” at any given time. A binary decision diagram is considered ‘alive’ if it is still needed to build binary decision diagrams for related fanout nodes. Notably, the order in which binary decision diagrams for the nodes in a circuit graph are built can cause an unnecessarily large number of binary decision diagrams to be alive at any given time. What is needed is a method to reduce the resource consumption in constructing binary decision diagrams by appropriately scheduling construction of binary decision diagrams to reduce the number of nodes that are alive at any given time.